\begin{tabbing}
$\forall$\=${\it sv}$:(Id$\rightarrow$($T$:Type $\times$ ($T$ + ($\mathbb{Q}\rightarrow$$T$)))), ${\it av}$:(Knd$\rightarrow$Type), ${\it dis}$:(Id$\rightarrow$Id$\rightarrow\mathbb{B}$),\+
\\[0ex]${\it cl}$:(Id$\rightarrow$($n$:$\mathbb{Z}$ $\times$ base{-}domain{-}type($n$))$\rightarrow$Realizer), ${\it fr}$, ${\it rfr}$:(Id$\rightarrow$Id$\rightarrow$(Knd List)),
\\[0ex]${\it sfr}$:(IdLnk$\rightarrow$Id$\rightarrow$(Knd List)), ${\it afr}$:(Id$\rightarrow$Knd$\rightarrow$((Id List) + Top)),
\\[0ex]${\it bfr}$:(Id$\rightarrow$Knd$\rightarrow$((IdLnk List) + Top)), $A$, $B$:Realizer.
\-\\[0ex]R{-}FeasibleWitness\=\{i:l\}\+
\\[0ex]($A$; ${\it sv}$; ${\it av}$; ${\it dis}$; ${\it cl}$; ${\it fr}$; ${\it sfr}$; ${\it rfr}$; ${\it afr}$; ${\it bfr}$)
\-\\[0ex]$\Rightarrow$ R{-}FeasibleWitness\=\{i:l\}\+
\\[0ex]($B$; ${\it sv}$; ${\it av}$; ${\it dis}$; ${\it cl}$; ${\it fr}$; ${\it sfr}$; ${\it rfr}$; ${\it afr}$; ${\it bfr}$)
\-\\[0ex]$\Rightarrow$ $A$ $\parallel$ $B$
\end{tabbing}